Search Results

Documents authored by Lodaya, Kamal

Document
DOI: 10.4230/LIPIcs.CSL.2018.28
An Algebraic Decision Procedure for Two-Variable Logic with a Between Relation

Authors: Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, and Howard Straubing

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
In earlier work (LICS 2016), the authors introduced two-variable first-order logic supplemented by a binary relation that allows one to say that a letter appears between two positions. We found an effective algebraic criterion that is a necessary condition for definability in this logic, and conjectured that the criterion is also sufficient, although we proved this only in the case of two-letter alphabets. Here we prove the general conjecture. The proof is quite different from the arguments in the earlier work, and required the development of novel techniques concerning factorizations of words. We extend the results to binary relations specifying that a factor appears between two positions.
Cite as

Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, and Howard Straubing. An Algebraic Decision Procedure for Two-Variable Logic with a Between Relation. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{krebs_et_al:LIPIcs.CSL.2018.28,
  author =	{Krebs, Andreas and Lodaya, Kamal and Pandya, Paritosh K. and Straubing, Howard},
  title =	{{An Algebraic Decision Procedure for Two-Variable Logic with a Between Relation}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{28:1--28:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.28},
  URN =		{urn:nbn:de:0030-drops-96953},
  doi =		{10.4230/LIPIcs.CSL.2018.28},
  annote =	{Keywords: two-variable logic, finite model theory, algebraic automata theory}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.FSTTCS.2010
LIPIcs, Volume 8, FSTTCS'10, Complete Volume

Authors: Kamal Lodaya and Meena Mahajan

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
LIPIcs, Volume 8, FSTTCS'10, Complete Volume
Cite as

IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Proceedings{lodaya_et_al:LIPIcs.FSTTCS.2010,
  title =	{{LIPIcs, Volume 8, FSTTCS'10, Complete Volume}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010},
  URN =		{urn:nbn:de:0030-drops-41027},
  doi =		{10.4230/LIPIcs.FSTTCS.2010},
  annote =	{Keywords: Software/Program Verification, Models of Computation, Modes of Computation, Complexity Measures and Classes, Nonnumerical Algorithms and Problems pecifying and Verifying and Reasoning about Program}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.FSTTCS.2010.i
Frontmatter, Table of Contents, Preface, Conference Organization, Author Index

Authors: Kamal Lodaya and Meena Mahajan

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
This proceedings volume has the papers presented at the 30th annual conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), held at the Institute of Mathematical Sciences (IMSc), Chennai, during 15–18 December 2010. The conference attracted 128 submissions from 35 countries in 6 continents, most of them of very high quality. We thank the authors who submitted for making this such a competitive conference. The PC succeeded in obtaining the help of 216 external reviewers, in all producing 400 referee reports which were of immeasurable help in deciding the 38 contributed papers which have made it to this publication.
Cite as

IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. i-xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{lodaya_et_al:LIPIcs.FSTTCS.2010.i,
  author =	{Lodaya, Kamal and Mahajan, Meena},
  title =	{{Frontmatter, Table of Contents, Preface, Conference Organization, Author Index}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{i--xvi},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.i},
  URN =		{urn:nbn:de:0030-drops-28475},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Conference Organization, Author Index}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2009.2331
Modelchecking counting properties of 1-safe nets with buffers in paraPSPACE

Authors: M. Praveen and Kamal Lodaya

Published in: LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)

Abstract
We consider concurrent systems that can be modelled as $1$-safe Petri nets communicating through a fixed set of buffers (modelled as unbounded places). We identify a parameter $\ben$, which we call ``benefit depth'', formed from the communication graph between the buffers. We show that for our system model, the coverability and boundedness problems can be solved in polynomial space assuming $\ben$ to be a fixed parameter, that is, the space requirement is $f(\ben)p(n)$, where $f$ is an exponential function and $p$ is a polynomial in the size of the input. We then obtain similar complexity bounds for modelchecking a logic based on such counting properties. This means that systems that have sparse communication patterns can be analyzed more efficiently than using previously known algorithms for general Petri nets.
Cite as

M. Praveen and Kamal Lodaya. Modelchecking counting properties of 1-safe nets with buffers in paraPSPACE. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 347-358, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{praveen_et_al:LIPIcs.FSTTCS.2009.2331,
  author =	{Praveen, M. and Lodaya, Kamal},
  title =	{{Modelchecking counting properties of 1-safe nets with buffers in paraPSPACE}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{347--358},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2331},
  URN =		{urn:nbn:de:0030-drops-23314},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2331},
  annote =	{Keywords: Petri nets, Coverability, Boundedness, paraPSPACE}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact